1.
msc diagrams: CW_answer(9) and CW_switch1(8)
INCONSISTENCY:
Matching formula: k9 = k8
Precondition 1: state (n9 , ringing k9) & rel (k9 , m9 , connected);
Precondition 2: rel (k8 , m8 , cw hold connect n8);
Post condition 1: rel (k9 , m9 , cw hold connect n9);
Post condition 2: rel (k8 , n8 , cw hold connect m8);
 
2.
msc diagrams: CW_answer(9) and CW_switch2(7)
INCONSISTENCY:
Matching formula: k9 = k7
Precondition 1: state(n9 , ringing k9) & rel (k9 , m9 , connected);
Precondition 2: rel (k7 , m7 , cw hold);
Post condition 1: rel (k9 , m9 , cw hold connect n9);
Post condition 2: rel (k7 , m7 , connected);

3.
msc diagrams: CW_answer(9) and CW_teardown2(4)
INCONSISTENCY:
Matching formula: k9 = k4
Precondition 1: state (n9 , ringing k9) & rel (k9 , m9 , connected);
Precondition 2: rel (k4 , m4 , cw hold connect n4);
Post condition 1: rel (k9 , m9 , cw hold connect n9);
Post condition 2: rel (k4 , n4 , cw hold);

4.
msc diagrams: CW_switch1(8) and CW_switch2(7)
INCONSISTENCY:
Matching formula: k8 = k7
Precondition 1: rel (k8 , m8 , cw hold connect n8);
Precondition 2: rel (k7 , m7 , cw hold);
Post condition 1: rel (k8 , n8 , cw hold connect m8);
Post condition 2: rel (k7 , m7 , connected);

5.
msc diagrams: CW_switch2(7) and CW_teardown2(4)
INCONSISTENCY:
Matching formula: k7 = k4
Precondition 1: rel (k7 , m7 , cw hold);
Precondition 2: rel (k4 , m4 , cw hold connect n4);
Post condition 1: rel (k7 , m7 , connected);
Post condition 2: rel (k4 , n4 , cw hold);

6.
msc diagrams: CW_teardown1(6) and CW_teardown2(4)
INCONSISTENCY:
Matching formula: m6 = m4
Precondition 1: rel (k6 , n6 , cw hold connect m6);
Precondition 2: rel (k4 , m4 , cw hold connect n4);
Post condition 1: rel (k6 , n6 , connected);
Post condition 2: rel (k4 , n4 , cw hold);

7.
msc diagrams: CW_teardown1(6) and CW_teardown3(1)
INCONSISTENCY:
Matching formula: m6 = k1
Precondition 1: rel (k6 , n6 , cw hold connect m6);
Precondition 2: rel (k1 , n1 , cw hold connect m1);
Post condition 1: rel (k6 , n6 , connected);
Post condition 2: state (m1 , diale) & state (n1 , diale);

8.
msc diagrams: CW_teardown2(4) and CW_teardown3(1)
INCONSISTENCY:
Matching formula: m4 = k1
Precondition 1: rel (k4 , m4 , cw hold connect n4);
Precondition 2: rel (k1 , n1 , cw hold connect m1);
Post condition 1: rel (k4 , n4 , cw hold);
Post condition 2: state (m1 , diale) & state (n1 , diale);